Inference at * 1 1 0 
Iof proof for Lemma add cancel in lt:

.....assertion..... NILNIL

1. a : 
2. b : 
3. n : 
4. (a+n) < (b+n)
  (a+n+(-n)) < (b+n+(-n)) 

latex

 by PERMUTE{1:n, 2:n, 3:n, 2:n, 4:n, 5:n} 

latex

 1: .....wf..... NILNIL

 1:   a+n  
 2: .....wf..... NILNIL

 2:   (-n)  
 3: .....wf..... NILNIL

 3:   b+n  
 4: 

 4:   (a+n) < (b+n)
 5: 

 5:   (-n)  (-n)
 .

Definitions	t  T, f(a), s = t, x:AB(x), A  B, -n, n+m, a < b, , P  Q, x:A. B(x)
Lemmas	add functionality wrt lt